T:Type, l1, l2:(T List). l1 || l2  (l:T List. (l1  l & l2  l)) 

latex

Definitions	P  Q, P  Q, P  Q, l1 || l2, x:A. B(x), P & Q, , l1  l2, x:A. B(x), t  T, P  Q
Lemmas	common iseg compat, iseg weakening, iseg wf, compat wf